Nuprl Lemma : equal_symmetry
9,38
postcript
pdf
T
:Type,
x
,
y
:
T
. (
x
=
y
)
(
y
=
x
)
latex
ProofTree
Definitions
,
t
T
,
P
Q
,
P
Q
,
P
Q
,
P
Q
,
x
:
A
.
B
(
x
)
origin
T:Type, x,y:T. (x = y) 
(y = x)
T:Type, x,y:T. (x = y) (y = x)
T Q Q
Q Qx:A. B(x)